package adder;

import java.util.ArrayList;

import JaCoP.constraints.And;
import JaCoP.constraints.Constraint;
import JaCoP.constraints.IfThen;
import JaCoP.constraints.IfThenElse;
import JaCoP.constraints.Not;
import JaCoP.constraints.Or;
import JaCoP.constraints.Reified;
import JaCoP.constraints.XeqC;
import JaCoP.constraints.XeqY;
import JaCoP.constraints.XneqY;
import JaCoP.core.BooleanVar;
import JaCoP.core.IntVar;
import JaCoP.core.Store;
import JaCoP.search.DepthFirstSearch;
import JaCoP.search.IndomainMin;
import JaCoP.search.InputOrderSelect;
import JaCoP.search.Search;
import JaCoP.search.SelectChoicePoint;

public class FullAdder {
	protected BooleanVar A, B, C, CoutInverse, SumInverse, One, Zero; // i/o
																		// signals
	protected Store store;

	public FullAdder() {
		store = new Store();
		A = new BooleanVar(store, "A");
		B = new BooleanVar(store, "B");
		C = new BooleanVar(store, "C");
		CoutInverse = new BooleanVar(store, "CoutInverse");
		SumInverse = new BooleanVar(store, "SumInverse");
		One = new BooleanVar(store, "One", 1, 1);
		Zero = new BooleanVar(store, "Zero", 0, 0);
		store.impose(new XeqC(One, 1));
		BooleanVar[] searchVars = new BooleanVar[5];
		searchVars[0] = A;
		searchVars[1] = B;
		searchVars[2] = C;
		searchVars[3] = CoutInverse;
		searchVars[4] = SumInverse;

		setupInverseCarryModule();

		setupInverseSumModule();

		Search<IntVar> search = new DepthFirstSearch<IntVar>();
		SelectChoicePoint<IntVar> select = new InputOrderSelect<IntVar>(store,
				searchVars, new IndomainMin<IntVar>());

		search.getSolutionListener().searchAll(true);
		search.getSolutionListener().recordSolutions(true);

		// for (int i = 1; i <= search.getSolutionListener().solutionsNo(); i++)
		// {
		// System.out.print("Solution " + i + ": ");
		// for (int j = 0; j < search.getSolution(i).length; j++)
		// 		System.out.print(search.getSolution(i)[j]);
		// 	System.out.println();
		// }

		//
		boolean result = search.labeling(store, select);

		// if (result)
		// System.out.println("Solution: " + v[0] + ", " + v[1] + ", " + v[2]
		// + " gives " + v[6] + ", " + v[7]);
		// else
		// System.out.println("*** No");
		for (int i = 0; i < 5; i++) {
			System.out.println("" + searchVars[i]);
		}
		System.out.println("------------------");
		search.getSolutionListener().printAllSolutions();
	}

	protected void setupInverseCarryModule() {
		// Left one
		ArrayList<BooleanVar> invCarryModVars = new ArrayList<BooleanVar>();
		for (int i = 0; i < 5; i++) {
			invCarryModVars.add(new BooleanVar(store, "CV:" + i));
		}
		connect(A, One, invCarryModVars.get(0), true);
		connect(B, One, invCarryModVars.get(0), true);
		connect(C, invCarryModVars.get(0), CoutInverse, true);
		connect(C, CoutInverse, invCarryModVars.get(1), false);
		connect(A, invCarryModVars.get(1), Zero, false);
		connect(B, invCarryModVars.get(1), Zero, false);
		connect(B, Zero, invCarryModVars.get(3), false);
		connect(A, invCarryModVars.get(3), CoutInverse, false);
		connect(B, One, invCarryModVars.get(4), true);
		connect(A, invCarryModVars.get(4), CoutInverse, true);
	}

	protected void setupInverseSumModule() {
		// Right one
		ArrayList<BooleanVar> invSumModVars = new ArrayList<BooleanVar>();
		for (int i = 0; i < 7; i++) {
			invSumModVars.add(new BooleanVar(store, "SV:" + i));
		}
		// right-hand side of the right circuit
		connect(A, One, invSumModVars.get(1), true);
		connect(B, invSumModVars.get(1), invSumModVars.get(2), true);
		connect(C, invSumModVars.get(2), SumInverse, true);
		connect(C, SumInverse, invSumModVars.get(3), false);
		connect(B, invSumModVars.get(3), invSumModVars.get(4), false);
		connect(A, invSumModVars.get(4), Zero, false);

		// left-hand side of the right circuit
		connect(A, One, invSumModVars.get(5), true);
		connect(B, One, invSumModVars.get(5), true);
		connect(C, One, invSumModVars.get(5), true);
		connect(CoutInverse, invSumModVars.get(5), SumInverse, true);
		connect(CoutInverse, SumInverse, invSumModVars.get(6), false);
		connect(A, invSumModVars.get(6), Zero, false);
		connect(B, invSumModVars.get(6), Zero, false);
		connect(C, invSumModVars.get(6), Zero, false);
	}

	protected void connect(BooleanVar extBoolVar, BooleanVar in,
			BooleanVar out, boolean inverse) {
		if (inverse) {
			BooleanVar temp = new BooleanVar(store, extBoolVar.id + "inversed");
			store.impose(new XneqY(temp, extBoolVar));
			extBoolVar = temp;
		}
		// And bothTrue = new And(new XeqY(extBoolVar, in), new XeqC(in, 1));
		// store.impose(new IfThen(bothTrue, new XeqC(out, 1)));
		// b =1 => (x=y)
		// x, y och b som switchg
		store.impose(new IfThen(new XeqC(extBoolVar, 1), new XeqY(in, out)));
	}
}
